k:FinProbSpace, n:, X, Y:RandomVariable(k;n). X  Y  RandomVariable(k;n) 

latex

Definitions	t  T, , x:A. B(x), ||as||, P & Q, i  j < k, a < b, P  Q, False, A, A  B, , {x:A| B(x)} , {i..j}, #$n, Void, x:AB(x), (x  l), r  s, x. t(x), xL. P(x), l[i], a  j < b. E(j), s = t, x:A  B(x), type List, , Type, f(a), q_le(r;s), if b then t else f fi , x.A(x), A  B, RandomVariable(p;n), FinProbSpace
Lemmas	ifthenelse wf, q le wf, nat wf, qsum wf, select wf, int seg wf, l all wf2, qle wf, int inc rationals, l member wf, length wf1, rationals wf